mcsta/modest mcsta crowds.jani -E TotalRuns=5,CrowdSize=20 --props positive -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --alg OptimisticValueIteration --epsilon 5e-2 --width 5e-2 --relative-width --p0 --p1
crowds.jani:model: info: crowds is a DTMC model.
crowds.jani: info: Need 40 bytes per state.
crowds.jani: warning: The probabilities for a transition do not sum up to 1. Results will likely be affected by floating-point errors.
crowds.jani: info: Explored 2018094 states for TotalRuns=5, CrowdSize=20.
Peak memory usage: 687 MB
Analysis results for crowds.jani
Experiment TotalRuns=5, CrowdSize=20
+ State space exploration
State size: 40 bytes
States: 2018094
Transitions: 2018094
Branches: 7224834
Rate: 396249 states/s
Time: 5.4 s
+ Property positive
Probability: 0.08759324776122866
Bounds: [0.08527397438027368, 0.08991252114218365]
Time: 1.2 s
+ Precomputations
Min. prob. 0 states: 1745849
Time for min. prob. 0 states: 0.5 s
Min. prob. 1 states: 3542
Time for min. prob. 1 states: 0.1 s
+ Essential states
Iterations: 2
Essential states: 212522
Transitions: 212522
Branches: 1700162
Time: 0.2 s
+ Optimistic value iteration
Total iterations: 25
Verif. attempts: 2
Verif. iterations: 7
Final epsilon: 0.01278391874944362
Time: 0.4 s
Exported results to file "/out.txt".